min2(0, y) -> 0
min2(x, 0) -> 0
min2(s1(x), s1(y)) -> s1(min2(x, y))
max2(0, y) -> y
max2(x, 0) -> x
max2(s1(x), s1(y)) -> s1(max2(x, y))
twice1(0) -> 0
twice1(s1(x)) -> s1(s1(twice1(x)))
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
p1(s1(x)) -> x
f2(s1(x), s1(y)) -> f2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
↳ QTRS
↳ DependencyPairsProof
min2(0, y) -> 0
min2(x, 0) -> 0
min2(s1(x), s1(y)) -> s1(min2(x, y))
max2(0, y) -> y
max2(x, 0) -> x
max2(s1(x), s1(y)) -> s1(max2(x, y))
twice1(0) -> 0
twice1(s1(x)) -> s1(s1(twice1(x)))
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
p1(s1(x)) -> x
f2(s1(x), s1(y)) -> f2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
F2(s1(x), s1(y)) -> P1(twice1(min2(x, y)))
F2(s1(x), s1(y)) -> TWICE1(min2(x, y))
F2(s1(x), s1(y)) -> MIN2(s1(x), s1(y))
MIN2(s1(x), s1(y)) -> MIN2(x, y)
F2(s1(x), s1(y)) -> MIN2(x, y)
F2(s1(x), s1(y)) -> -12(max2(s1(x), s1(y)), min2(s1(x), s1(y)))
-12(s1(x), s1(y)) -> -12(x, y)
F2(s1(x), s1(y)) -> F2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
MAX2(s1(x), s1(y)) -> MAX2(x, y)
F2(s1(x), s1(y)) -> MAX2(s1(x), s1(y))
TWICE1(s1(x)) -> TWICE1(x)
min2(0, y) -> 0
min2(x, 0) -> 0
min2(s1(x), s1(y)) -> s1(min2(x, y))
max2(0, y) -> y
max2(x, 0) -> x
max2(s1(x), s1(y)) -> s1(max2(x, y))
twice1(0) -> 0
twice1(s1(x)) -> s1(s1(twice1(x)))
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
p1(s1(x)) -> x
f2(s1(x), s1(y)) -> f2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F2(s1(x), s1(y)) -> P1(twice1(min2(x, y)))
F2(s1(x), s1(y)) -> TWICE1(min2(x, y))
F2(s1(x), s1(y)) -> MIN2(s1(x), s1(y))
MIN2(s1(x), s1(y)) -> MIN2(x, y)
F2(s1(x), s1(y)) -> MIN2(x, y)
F2(s1(x), s1(y)) -> -12(max2(s1(x), s1(y)), min2(s1(x), s1(y)))
-12(s1(x), s1(y)) -> -12(x, y)
F2(s1(x), s1(y)) -> F2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
MAX2(s1(x), s1(y)) -> MAX2(x, y)
F2(s1(x), s1(y)) -> MAX2(s1(x), s1(y))
TWICE1(s1(x)) -> TWICE1(x)
min2(0, y) -> 0
min2(x, 0) -> 0
min2(s1(x), s1(y)) -> s1(min2(x, y))
max2(0, y) -> y
max2(x, 0) -> x
max2(s1(x), s1(y)) -> s1(max2(x, y))
twice1(0) -> 0
twice1(s1(x)) -> s1(s1(twice1(x)))
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
p1(s1(x)) -> x
f2(s1(x), s1(y)) -> f2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
-12(s1(x), s1(y)) -> -12(x, y)
min2(0, y) -> 0
min2(x, 0) -> 0
min2(s1(x), s1(y)) -> s1(min2(x, y))
max2(0, y) -> y
max2(x, 0) -> x
max2(s1(x), s1(y)) -> s1(max2(x, y))
twice1(0) -> 0
twice1(s1(x)) -> s1(s1(twice1(x)))
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
p1(s1(x)) -> x
f2(s1(x), s1(y)) -> f2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
-12(s1(x), s1(y)) -> -12(x, y)
POL(-12(x1, x2)) = 2·x1 + x2
POL(s1(x1)) = 2 + 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
min2(0, y) -> 0
min2(x, 0) -> 0
min2(s1(x), s1(y)) -> s1(min2(x, y))
max2(0, y) -> y
max2(x, 0) -> x
max2(s1(x), s1(y)) -> s1(max2(x, y))
twice1(0) -> 0
twice1(s1(x)) -> s1(s1(twice1(x)))
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
p1(s1(x)) -> x
f2(s1(x), s1(y)) -> f2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
TWICE1(s1(x)) -> TWICE1(x)
min2(0, y) -> 0
min2(x, 0) -> 0
min2(s1(x), s1(y)) -> s1(min2(x, y))
max2(0, y) -> y
max2(x, 0) -> x
max2(s1(x), s1(y)) -> s1(max2(x, y))
twice1(0) -> 0
twice1(s1(x)) -> s1(s1(twice1(x)))
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
p1(s1(x)) -> x
f2(s1(x), s1(y)) -> f2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TWICE1(s1(x)) -> TWICE1(x)
POL(TWICE1(x1)) = 2·x1
POL(s1(x1)) = 1 + 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
min2(0, y) -> 0
min2(x, 0) -> 0
min2(s1(x), s1(y)) -> s1(min2(x, y))
max2(0, y) -> y
max2(x, 0) -> x
max2(s1(x), s1(y)) -> s1(max2(x, y))
twice1(0) -> 0
twice1(s1(x)) -> s1(s1(twice1(x)))
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
p1(s1(x)) -> x
f2(s1(x), s1(y)) -> f2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
MAX2(s1(x), s1(y)) -> MAX2(x, y)
min2(0, y) -> 0
min2(x, 0) -> 0
min2(s1(x), s1(y)) -> s1(min2(x, y))
max2(0, y) -> y
max2(x, 0) -> x
max2(s1(x), s1(y)) -> s1(max2(x, y))
twice1(0) -> 0
twice1(s1(x)) -> s1(s1(twice1(x)))
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
p1(s1(x)) -> x
f2(s1(x), s1(y)) -> f2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MAX2(s1(x), s1(y)) -> MAX2(x, y)
POL(MAX2(x1, x2)) = 2·x1 + x2
POL(s1(x1)) = 2 + 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
min2(0, y) -> 0
min2(x, 0) -> 0
min2(s1(x), s1(y)) -> s1(min2(x, y))
max2(0, y) -> y
max2(x, 0) -> x
max2(s1(x), s1(y)) -> s1(max2(x, y))
twice1(0) -> 0
twice1(s1(x)) -> s1(s1(twice1(x)))
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
p1(s1(x)) -> x
f2(s1(x), s1(y)) -> f2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
MIN2(s1(x), s1(y)) -> MIN2(x, y)
min2(0, y) -> 0
min2(x, 0) -> 0
min2(s1(x), s1(y)) -> s1(min2(x, y))
max2(0, y) -> y
max2(x, 0) -> x
max2(s1(x), s1(y)) -> s1(max2(x, y))
twice1(0) -> 0
twice1(s1(x)) -> s1(s1(twice1(x)))
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
p1(s1(x)) -> x
f2(s1(x), s1(y)) -> f2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MIN2(s1(x), s1(y)) -> MIN2(x, y)
POL(MIN2(x1, x2)) = 2·x1 + x2
POL(s1(x1)) = 2 + 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
min2(0, y) -> 0
min2(x, 0) -> 0
min2(s1(x), s1(y)) -> s1(min2(x, y))
max2(0, y) -> y
max2(x, 0) -> x
max2(s1(x), s1(y)) -> s1(max2(x, y))
twice1(0) -> 0
twice1(s1(x)) -> s1(s1(twice1(x)))
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
p1(s1(x)) -> x
f2(s1(x), s1(y)) -> f2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
F2(s1(x), s1(y)) -> F2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))
min2(0, y) -> 0
min2(x, 0) -> 0
min2(s1(x), s1(y)) -> s1(min2(x, y))
max2(0, y) -> y
max2(x, 0) -> x
max2(s1(x), s1(y)) -> s1(max2(x, y))
twice1(0) -> 0
twice1(s1(x)) -> s1(s1(twice1(x)))
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
p1(s1(x)) -> x
f2(s1(x), s1(y)) -> f2(-2(max2(s1(x), s1(y)), min2(s1(x), s1(y))), p1(twice1(min2(x, y))))